IBEX_ROOT=../..

SAIL=sail

SAIL_RISCV_MODEL_DIR=${LOWRISC_SAIL_RISCV_SRC}/model

include Sources.mk

PSGEN_SRCS=thm/btype.proof thm/ibex.proof thm/mem.proof thm/riscv.proof
PSGEN_FLAGS=-root riscv -task

SAIL_EXTRA_SRCS=../spec/main.sail

SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv-nomem -Oconstant_fold -memo-z3 \
	-sv-unreachable translate -sv-unreachable lookup_TLB -sv-unreachable translate_tlb_miss -sv-unreachable translate_tlb_hit -sv-unreachable pt_walk \
	-sv-fun2wires 2:read_ram \
	-sv-fun2wires 2:write_ram \
	-sv-fun2wires wX \
	-sv-fun2wires 2:rX \

# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
# and then generate a filelist for jasper to ingest.
# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
#   JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
.PHONY: fusesoc
fusesoc:
	mkdir -p build/fusesoc
	fusesoc \
	  --cores-root $(IBEX_ROOT) \
	  run \
	  --build-root build/fusesoc \
	  --tool vcs \
	  --setup \
	  lowrisc:ibex:ibex_formal:0.1

.PHONY: sv
sv:
	mkdir -p build
	python3 buildspec.py header > build/ibexspec_instrs.sv
	cd build && $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) $(SAIL_SV_FLAGS) `cd .. && python3 buildspec.py unreachables` -o ibexspec
	python3 spec/fix_pmp_bug.py
	python3 buildspec.py unreachable_loc_hack

.PHONY: psgen
psgen:
	mkdir -p build
	psgen $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen.sv -tcl-out build/psgen.tcl

.PHONY: jg
jg: fusesoc psgen sv
	jg verify.tcl -allow_unsupported_OS -acquire_proj

# The following default target is intended for regressions / unattended runs.
.PHONY: all
all: fusesoc psgen sv
	jg verify.tcl -allow_unsupported_OS -acquire_proj -no_gui --- "prove_no_liveness"

################################################################################

.PHONY: clean
clean:
	rm -rf build/
	rm -rf jgproject/
	rm -rf jgproofs/
